e[e1,e2).P(e) == e:es-E(es). es-le(es; e1; e)  es-locl(es; e; e2)  P(e) 

latex

---

clarification:

alle from es in [e1;e2).P(e) == e:es-E(es). es-le(es; e1; e)  es-locl(es; e; e2)  P(e) 

latex

Definitions	e[e1,e2).P(e), x:A. B(x), es-E(es), es-le(es; e; e'), P  Q, es-locl(es; e; e')
FDL editor aliases	alle-between1